feat(semantics): evaluate KerML Rationals exactly - #838

What and why

A KerML Rational is now evaluated as a rational number instead of an IEEE binary64:
0.1 + 0.2 == 0.3 is true, 1 / 3 is the Rational 1/3, numer(rat(1, 3)) is 1.
Real stays binary64. docs/project/exact-rational-evaluation.md, which earlier declined this, is
rewritten as the record of the new decision; its pilot probes are kept as the documented
divergence from the pilot.

• semantics.Value gains an exact ValRational: lowest terms, positive denominator, inline
  (int64 numerator / uint32 denominator) when it fits, an immutable big.Rat otherwise.
  Integers stay ValInt; an Integer beyond int64 is now a big.Rat over one.
• Decimal and exponent literals parse exactly (semantics.ParseRational); Integer / is the exact
  quotient (replaces the once-rounded IntQuotient); + - * /, **/^ with an Integer exponent,
  comparisons, rat, numer, denom, gcd, abs, floor, round, max, min, sum,
  product, ToString, ToRational, ToInteger are exact.
• Size budget: numerator + denominator bits beyond DefaultMaxIntegerBits (shared with Integers)
  is semantics.ErrRationalSizeLimit, never a rounding; powers are refused from a lower bound
  before computing. A harmonic accumulation stops with that typed error.
• Printing: terminating decimals print as decimals in the layout a Real prints in (0.3, 2.0,
  1.5e-05); any other as numer/denom (1/3). Values that were already binary fractions print
  unchanged in REPL, JSON and traces.
• Real boundary (semantics.RealOf): a value written to a Real feature (holdAsReal),
  RealFunctions operands, and a Rational meeting a binary64 Real in arithmetic are rounded to the
  nearest double once. sqrt, trig, exp, ln, non-Integer ** stay binary64.
  RealFunctions::sum/product hold every magnitude as a Real, an Integer quantity's included
  (RealFunctions::sum((1 [m], 2 [m])) is 3.0 [m]), as they already did for plain Integers.
• Comparison (semantics.CompareReal): == != < <= > >= between a Rational and a binary64 Real
  compare the Rational's nearest double with the Real, the same rounding mixed arithmetic does,
  so a binding to a Real feature holds (x : Real = 0.1; x == 0.1 and rat(1, 3) == 1.0 / 3.0
  are true). A Rational past the binary64 range compares as ±Inf; NaN is unordered as before.
  Rational vs Rational stays exact, and so does Integer vs anything (CompareIntReal). Evaluator,
  runtime, set membership, query equality, solver replay and -compile share the rule. A
  Real-typed accumulation therefore stays binary64 and never reaches the Rational budget.
• Quantities/units: scale factors compose exactly while their terms are whole and within 2^53
  (0.1 [m] + 1 [mm] is exactly 0.101 [m]).
• Boundaries:
  • gRPC: additive Rational message in Value.rational_value, Quantity.rational_magnitude,
    DocumentValue.rational_value, negotiated by a new rational_values capability exactly as
    big_int_values. Answers are canonical: a binary64-exact Rational crosses as real_value,
    any other as rational_value. Inputs: a client sends every exact Rational as
    rational_value to a service advertising rational_values, and the service reads any
    lowest-terms rational_value (a binary64-exact one included) as that exact Rational; an
    inbound real_value is always a Real. Toward an older service a client rewrites a
    binary64-exact Rational as real_value and refuses any other, naming the capability; a
    service answering a client without the capability refuses (UNIMPLEMENTED), never a nearest
    double. Non-lowest-terms encodings are rejected (semantics.LowestTermsRational).
  • JSON: "rationalValue": {"numerator": "1", "denominator": "3"} / "rationalMagnitude".
  • Clients: Go opensysml.Rational, Python fractions.Fraction (generated classes type
    Rational features Fraction), Node {kind: "rational", numerator: bigint, denominator: bigint}, Java/Rust numerator–denominator pairs, Julia Rational{BigInt}, MATLAB decimal-string
    struct; each declares rational_values. Client value equality (Node valuesEqual, Java
    sameValue, Rust same_value, Julia same_value) follows the same comparison rule, so a
    set holding 1/3 and 1.0 / 3.0 is refused as a duplicate.
  • RDF: decimal literal → xsd:decimal; exponent literal → xsd:double only when a double holds
    it exactly, otherwise exact xsd:decimal. Round trip is exact.
  • SMT: replay is exact for Integer/Rational arithmetic; only arithmetic a binary64 Real takes
    part in is replayed and marked rounded (Query.Rounded). Census over all fixtures and corpora:
    6 queries remain marked rounded, all genuinely inexact.
  • sysml -compile: exact constants are folded; a single operation over binary64-exact values is
    compiled with guards; an Integer quotient compared with a whole number is compared exactly.
    An Integer to a negative literal power is the exact quotient, rounded once where it reaches a
    Real; one below the least Real fails as in the interpreter. A record attribute typed Real
    with a decimal default (attribute z : Real default 0.1;) holds that default rounded once,
    as the interpreter does.
• Opt-in lint rounded-real-literal (off by default): a decimal or exponent literal written to a
  Real feature that binary64 cannot hold exactly (attribute x : Real = 0.1;) warns and names the
  double it becomes (0.10000000000000001); 0.25, Integers, computed values and Rational
  features stay silent. Switch it on with sysml -enable-lint rounded-real-literal,
  %lint rounded-real-literal on, the LSP setting enabledLints, or model.WithEnabledLints;
  disabling wins over enabling. The gRPC service reports only on-by-default lints.

Still refused, and why: sysml -compile refuses — with a typed error naming the construct —
a Rational parameter, a * 0.1 over a variable, (a * 0.5) ** 2, a / 3 < 0.1, a ** -1 * 3, and collection
operations over exact Rationals, because compiled code holds numbers as int64/binary64 and these
would need more than one rounding. A Go Real parameter given an Integer meets an exact Rational only at run time, so there the
program fails with the same message. Arithmetic over an infinity remains a typed error, as for
LiteralInfinity today.

Two policy choices the specification does not settle, recorded as tool-defined in the
evaluation record:

1. Rational vs binary64 Real comparison is at Real precision (the Rational rounded once), as
   above. Exact comparison would make x : Real = 0.1; x == 0.1 false and break the equality a
   binding asserts (KerML §7.4.9), since holdAsReal rounds the bound value.
2. Wire input: exact Rationals are sent as rational_value under rational_values; an inbound
   real_value is always a Real; runtime semantics do not depend on the wire form.

Specification basis

• KerML 1.0 §9.3.2.2.8: "Rational is the type of rational numbers, extended with values for
  positive and negative infinity"; §9.3.2.2.9: Real "includes both rational and irrational numbers".
• §8.3.4.8.13 and §8.4.4.9.2: "the result of a LiteralRational is actually always classified in
  the KerML DataType Rational" — a finite decimal names a rational exactly.
• RationalFunctions.kerml (§9.4.10) and IntegerFunctions.kerml (§9.4.11), vendored under
  internal/workspace/libs: the declared result types decide classification — Integer / returns
  Rational, so 6 / 3 is the Rational 2 (istype Integer is false); floor, round,
  numer, denom, gcd, Integer + - * % ** return Integer.
• RationalFunctions::'**' declares y: Rational, but a non-Integer exponent has in general an
  irrational result, so only Integer exponents are exact; others are RealFunctions::'**'.
• KerML §7.4.9: a binding connector's two ends hold equal values — the reason comparison with a
  binary64 Real is at Real precision.
• Silent (decided and documented): representation, size bound, Real precision, how a Rational
  meets a binary64 Real, the wire form of an input, print form. UML/fUML/PSSM say nothing about KerML Rationals.

docs/project/spec-compliance.md: new/updated rows for literals, arithmetic, representation,
printing, the Real boundary, every wire boundary, RDF, -compile, rat/numer/denom,
floor/round, Integer /, solver replay and rounded marking.

Pilot differs by design. The pinned pilot holds LiteralRational as a Java double. The ten
probes are committed as tools/referee/exec/testdata/cases/exact_rationals.cases under a new
by-design: <clause> marker; five land in a new differs-by-design bucket with the clause beside
both raw outputs (0.1 + 0.2 == 0.3, 0.1 + 0.2 <= 0.3, 0.3 < 0.1 + 0.2,
(1.0 / 49.0) * 49.0 == 1.0, ten-fold 0.1 sum == 1.0), five agree within the harness's
two-decimal tolerance. Referee run against develop (446 cases) and this branch (456):
agree 212→217 · differs-by-design 0→5, every other bucket unchanged (disagree 29,
pilot-error 5, both-error 16, …); a per-case comparison of the two reports shows none of the
446 existing cases moved bucket. The stale totals in pilot-execution-referee.md and the
referee skill are updated to the measured ones.

How it was verified

Four-layer tests: golden AST fixture; conformance
action_exact_rational_accumulation.sysml + .expected.json; golden trace
action_exact_rational_accumulation.trace.golden; robustness_exact_rational_test.go
(TestRuntimeRobustnessExactRational: denominator growth beyond a lowered budget, a power and a
literal beyond the size budget, division by zero — each a typed error);
robustness_rational_real_comparison_test.go (TestRuntimeRobustnessRationalRealComparison:
Rational vs NaN, vs ±Inf, a Rational beyond the binary64 range vs a large Real, set membership,
and a 1000-step Real accumulation of 0.01 under a lowered budget). Conformance
instance_real_binding_meets_rational (binding equality, rat(1,3) == 1.0/3.0, rat(1,4) == 0.25)
and action_real_accumulation_stays_binary64. gRPC conformance covers both wire directions
(evaluate_calc_rational_wire*, execute_action_rational_input_meets_rational,
execute_action_real_input_meets_rational), as do the Python, Node, Julia, Rust, Java and MATLAB
client tests. -compile fixtures cover each comparison operator against the nearest double and
refuse a literal beyond the Real range.
Semantics unit tests cover storage, parsing, formatting, arithmetic, and wire validation.

go build ./...                      ok
go vet ./...                        ok
gofmt -l .                          (empty)
make docs-check                     OK
python3 scripts/changelog.py check  ok
make lint (staticcheck + gosec)     ok
OPENSYSML_REQUIRE_TRAINING_CORPUS=1 OPENSYSML_REQUIRE_PILOT_CORPORA=1 \
OPENSYSML_REQUIRE_PILOT_LIBRARY_XMI=1 OPENSYSML_REQUIRE_PSSM_SUITE=1 \
  go test -count=1 ./...            all packages ok (corpus gates incl. TestCorpusRoundTrip,
                                    TestTrainingExamples*, TestPilotCorpora*, TestPSSMSuiteMigration,
                                    TestPilotLibraryXMI)
go test -count=1 ./... (tools)      ok
go test -race -count=1 ./internal/semantic/semantics ./internal/exec/runtime ./internal/exec/solve \
  ./internal/frontend/grpc ./internal/translate/codegen ./internal/doc/queryexec \
  ./client/opensysml ./tests/grpc   ok
TestRoundedCensus (z3)              6 marked rounded, 0 recoverable, 6 genuinely inexact
client/python pytest                1431 passed, 6 skipped
client/node typecheck, eslint, test 383 passed
client/java mvn test                BUILD SUCCESS
client/rust fmt, clippy -D warnings, cargo test   ok (all suites)
client/julia Pkg.test               ok

training_examples_expected.txt is untouched; no corpus or RDF ratchet moved. Locally, GNU Octave
6.4 lacks jsonencode/jsondecode, so only the MATLAB encoding and capability tests ran there;
the MATLAB/Octave CI job runs the full suite.
The browser REPL walkthroughs (docs/assets/repl-walkthroughs.json, checked by
TestBrowserREPLWalkthroughs) now expect 100 [SI::km] / 2 [SI::h] as the exact 125/9 [SI::'m/s'],
%calc Speed 42.195 [SI::km] 2 [SI::h] as 2813/480 [SI::'m/s'], and the RealFunctions::sum
rollup car.mass as 1300.0 [kg].

Benchmarks (develop vs this branch, interleaved, six samples each, benchstat):

The byte increase beyond int64 is the big.Rat-over-one representation; the harmonic loop is the
genuine cost of exactness (denominator of hundreds of bits), bounded by the size budget.

Checklist

• make test and make lint pass locally
• Tests added or updated for the change
• Documentation extended where it already covers the surface (see CONTRIBUTING.md)
• Changelog entry added as changes/unreleased/<slug>.<section>.md, not as an edit to CHANGELOG.md
• baselines regenerated and make docs-counts run if a gate count moved (compliance rows need nothing: the census is counted at docs build)
• No internal work-item labels (waves, slices, F4, K5) in the body, docs, or changelog

Link to Devin session: https://nasa-jpl-demo.devinenterprise.com/sessions/0fe9b9a0b2db4a9a8d398dd29dd3ec33
Open in Devin Desktop: https://nasa-jpl-demo.devinenterprise.com/desktop/session/0fe9b9a0b2db4a9a8d398dd29dd3ec33?variant=devin
Requested by: @HuiJun